$\forall$$T$:Type, $l$:($T$ List), $a$,$x$,$y$:$T$.
\\[0ex]l\_before($x$; $y$; cons($a$; $l$); $T$) $\Leftarrow\!\Rightarrow$ ((($x$ = $a$) $\wedge$ ($y$ $\in$ $l$)) $\vee$ l\_before($x$; $y$; $l$; $T$))